(set-logic ALL)
(set-info :status unsat)
(set-option :miniscope-quant agg)
(set-option :macros-quant true)
(set-option :cegqi false)
(set-option :fmf-fun-rlv true)
(set-option :var-elim-quant false)
(declare-fun a (Int Bool Bool Int Int Int Int Int Int Int Bool Bool Int Bool Bool Bool Bool Bool Bool Bool) Bool)
(assert
 (forall ((bcm Int)
     (bq Bool)
     (bm Bool)
     (bcd Int)
     (bcs Int)
     (bce Int)
     (bn Int)
     (bf Int)
     (bt Int)
     (bd Int)
     (o Bool)
     (r Bool)
     (p Bool)
     (g Bool)
     (h Bool)
     (bi Bool)
     (bj Bool))
 (let ((k (= bd 0)))
  (let ((l (and (= bn bcm bcs) k (= bcd bcs))))
  (= l (a bcm bq bm bn bd bcs bce bn bf bt p g bd o r p g h bi bj))))))
(assert (forall ((bcm Int)
         (bq Bool)
         (bm Bool)
         (bcn Int)
         (bcd Int)
         (bcs Int)
         (bce Int)
         (bn Int)
         (bf Int)
         (bt Int)
         (bp Bool)
         (bg Bool)
         (bd Int)
         (o Bool)
         (r Bool)
         (p Bool)
         (g Bool)
         (h Bool)
         (bi Bool)
         (bj Bool))
     (not (a bcm bq bm bcn bcd bcs bce bn bf bt bp bg bd o r p g h bi bj))))
(check-sat)
